COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	facts about lengths of lists
C00006 ENDMK
C⊗;
;facts about lengths of lists
;10s
(wipe-out)
(get-proofs set prf ekl sys)
(get-proofs minus prf ekl sys)

(proof length)

(decl length (type: |ground→ground|) (syntype: constant) 
      (unaryname: length))
(define length |∀u x.(length nil=0)∧length(x.u)=(length u)'|
        (use listinductiondef))
(label simpinfo) (label lengthdef)

(axiom |∀u.natnum(length u)|)
(label simpinfo)

(axiom |∀u.length u=0≡null u|)
(label simpinfo)

(axiom |∀u v.length (u**v)=length u+length v|)
(label lengthadd) (label simpinfo)

(axiom |∀x.length (x.nil)=1|)
(label simpinfo)
 
(axiom |∀u n.length(u)≤n∨n<length(u)|)
(label trichotomy2)

(axiom |∀u y.member(y,u)⊃0<length u|)
(label simpinfo)(label have_member)

(axiom |∀u y.member(y,u)⊃¬null u|)
(label simpinfo)(label have_member1)

(save-proofs length)